<HTML>
<HEAD>
<TITLE>Fast small truth tables</TITLE>
</HEAD>
<BODY>

<P>
<EM>Abstract</EM>:
This note describes how small Joy sets (of up to 32 members)
can be used to encode the lines in a truth table for
up to five propositions. This results in a surprisingly
simple method of providing truth table tests for the
modal status of formulas (or other modal predicates).
<P>
Contents:
<UL>
<LI><A HREF=#TOC-1>Truthfunctional and set-theoretic operations</A>
<LI><A HREF=#TOC-2>Set operations in Joy</A>
<LI><A HREF=#TOC-3>Truth tables for Joy postfix formulas</A>
<LI><A HREF=#TOC-4>Using minimally parenthesised infix notation</A>
<LI><A HREF=#TOC-5>Using Cambridge notation</A>
<LI><A HREF=#TOC-6>Other applications</A>
</UL>

<A NAME=TOC-1><H2>Truthfunctional and set-theoretic operations</H2></A>
<P>
Truth tables are the simplest way to determine the modal status of a formula:
if it is true in all lines then it is a tautology,
if it is false in all lines then it is a contradiction,
and if it is true in some lines and false in others then it is contingent.
The truthfunctional connectives are normally taken to operate
on the two truth values, true and false.
There is an obvious relationship between the connectives
in a formula and the set of lines in the truth table in which
the formula is true:
The set of lines in which the negation
of a formula is true is just the set-theoretic complement
of the lines in which the formula itself is true,
the set of lines in which the conjunction of two formulas
is true is just the set-theoretic intersection
of the lines in which both component formulas are true,
and so on.

<P>
Hence, instead of evaluating a formula line by line in the truth table,
one could just use the set-theoretic operations
to determine the set of lines in which the formula is true.
Whether this is efficient depends on the relative speed of the
truthfunctional (one-bit) operations and the set-theoretic
(many-bit) operations.
Most computers now have word-wide Boolean operations
and 32 or even more bits per word. 
and
So, set-theoretic operations on sets of up to 32 or even more
members are as efficient as are the truthfunctional operations.
This can be exploited for truth tables,
and it has the potential of improving performance
of small truth tables by a factor of up to 32,
and even higher for larger size words.
With 32 bits per word, a single word can codify the set of lines
of a truth table generated by five propositions (2^5 = 32).
<P>
Of course nothing can escape the eventual exponential explosion.
For six propositions the truth table has 2^6 = 64 lines,
and, as always, any additional proposition doubles the size.
So, a six proposition truth table would need to be encoded
in two words, and then it doubles.
However, the 32-fold increase in speed will hold no matter
how many words are needed for the truth table.
Moreover, computers with 64-bit words are already
becoming more common, and 128-bit words are not far off.
Indeed, some machines alredy have 128-bit registers,
and a few can operate on several such registers in one cycle.

<P>
The rest of this note illustrates the general principle,
using just one 32-bit word per truth table,
and hence is restricted to a maximum of 5 propositions per table.

<A NAME=TOC-2><H2>Set operations in Joy</H2></A>
<P>
The language Joy has as small sets of (generallly 32)
integers from 0 onwards (generally up to 31).
These integers can be taken to be the line numbers
of a truth table, starting with line number 0.

<P>
What is needed, for each atomic proposition,
is the set of line numbers of the lines in which that
proposition is true.
In the usual way of writing truth tables, these are the
five guide columns.
In setlib.joy, the standard Joy libray for (small and large) sets,
there is a module ss for small (32-bit) sets
which contains, among others, just the right definitions
for the current purpose.
These definitions are here reproduced for convenience:
<PRE>
    s1  == { 0  2  4  6  8 10 12 14 16 18 20 22 24 26 28 30 };
    s2  == { 0  1  4  5  8  9 12 13 16 17 20 21 24 25 28 29 };
    s4  == { 0  1  2  3  8  9 10 11 16 17 18 19 24 25 26 27 };
    s8  == { 0  1  2  3  4  5  6  7  8 17 18 19 20 21 22 23 };
    s16 == { 0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15 };
</PRE>

<P>
The names for these sets have been chosen because they are descriptive
for general use, but they are not customary in logic.
Moreover, since these sets are defined inside a module,
they would have to be referenced as ss.s1, ss.s2, ss.s4 and so on.
But this is easily overcome by some definitions,
chosing p, q, r and so on.
Also, it is necessary to load the setlib.joy library:
<PRE>
"setlib" libload.

DEFINE
  p == ss.s1; q == ss.s2; r == ss.s4; s == ss.s8; t == ss.s16.
</PRE>

<P>
Joy has the Boolean operators 'and', 'or' and 'not',
and they are defined for the two Boolean types of
truth values and (small) sets.
So these three can already be used for the operations
on sets of lines.

<P>
But in logic one frequently uses material implication
and material equivalence, and these operations will be needed.
In the definition below they have been chosen as say, 'imp' and 'iff'.
Also, a set of lines represents a tautology
if and only if it comprises all lines
if and only if it is the universal set.
In the definition below the predicate 'tautology'
is defined to be true if the complement of the set is  empty.
<PRE>
DEFINE
  imp == [not] dip or;
  iff == [imp] [swap imp] cleave and popd;
  tautology == not null
END
</PRE>

<A NAME=TOC-3><H2>Truth tables for Joy postfix formulas</H2></A>
<P>
No further definitions are needed.
The Joy interpreter can now read formulas in Joy postfix
notation and determine whether they are tautologies.
It does so simply by executing them and
then use tre 'tautology' predicate to determine
whether what is on top of the stack is
the unversal set.
<PRE>
p q imp p and  q  imp tautology.
true
p q imp q and  p  imp tautology.
false
p q or  p r imp  q s imp  and and   r s or   imp  tautology.
true
p q or  p r imp  q s imp  and and   r s and  imp  tautology.
false
</PRE>

<P>
A formula that is not a tautology is either contingent
or it is a contradiction.
It might be useful to have two more predicates for this.
But simpler still is to have a function 'modality'
which simply determines which of the three possibilities obtains.
<PRE>
DEFINE
  modality == 
	[ [ [null] "contradiction" ]
	  [ [not null] "tautology" ]
	  [ "contingent" ] ]
	cond
	popd
END
</PRE>
The use of this predicate is illustrated by the following
three similar looking stock examples.
<PRE>
p p not and   modality.
"contradiction"
p q not and   modality.
"contingent"
p p not  or   modality.
"tautology"
</PRE>
Here are some more examples:<BR>
<PRE>
p q imp p and  q  imp modality.
"tautology"
p q imp p and  q  imp not  modality.
"contradiction"
p q imp q and  p  imp modality.
"contingent"
p q imp q and  p  imp not  modality.
"contingent"
p q imp  p not q imp  iff  modality.
"contingent"
p q imp  q not p not imp  iff  modality.
"tautology"
p q or  p r imp  q s imp  and and   r s or   imp  modality.
"tautology"
p q or  p r imp  q s imp  and and   r s or   imp  not  modality.
"contradiction"
p q or  p r imp  q s imp  and and   r s and  imp  modality.
"contingent"
p q or  p r imp  q s imp  and and   r s and  imp  not  modality.
"contingent"
</PRE>

<A NAME=TOC-4><H2>Using minimally parenthesised infix notation</H2></A>
<P>
Reverse Polish notation may be second nature to Joy programmers,
but it is not to logicians who would prefer a more familiar
notation.
The Joy system has a library symlib.joy for symbolic manipulation.
It includes many translators from various notations to others.
One familiar notation is infix, with  precedences
for the binary operators to minimise the need for parentheses.
The translating function to reverse Polish is called Min2Rev.
But the library has to loaded,
and it needs to be told which operators are to be used, and what
their precedences are:
<PRE>
"symlib"  libload.

DEFINE
  unops == [not];
  bin3ops == [and];
  bin2ops == [or];
  bin1ops == [imp iff];
END
</PRE>
In the following the first item is a Joy tree representing
a formula in minimally parenthesised infix notation.
This is then translated into a quotation of the same
formula in Joy notation. The i combinator then executes
the quotation, with the result that the top of the stack is now
the set of lines in the truth table in which that formula is true.
The tautology predicate then determines whether that set
is the set of all lines, just as before.
<PRE>
[ [p imp q] and p  imp  q ] Min2Rev i tautology.
true
[ [p imp q] and q  imp  p ] Min2Rev i tautology.
false
</PRE>
But it is more convenient not to have to specify the
translation operator and the i combinator every time:<BR>
<PRE>
DEFINE
  Mtautology == Min2Rev i tautology;
  Mmodality  == Min2Rev i modality
END
</PRE>
<PRE>
[ [p imp q] iff [not p or q] ]  Mtautology.
true
[ [p imp q] iff [not q or p] ]  Mtautology.
false
[ [p or q] and [p imp r] and [q imp s]  imp  [r or s] ]  Mmodality.
"tautology"
[ [p imp q] iff [q imp p] ]  Mmodality.
"contingent"

[ [ [p imp q] and [q imp r] and [r imp s] and [s imp t] ]
  imp [p imp t] ]
Mmodality.
"tautology"

[ [[p imp q] and [q imp r] and [s imp r] and [s imp t]]
  imp  [p imp t] ]
Mmodality.
"contingent"
</PRE>

<A NAME=TOC-5><H2>Using Cambridge notation</H2></A>
<P>
In the symlib.joy library there is also a translator from
Cambridge (or Lisp) style notation to Joy notation.
The translator is called Cam2Rev, and it is useful to
define the following operators straight away:
<PRE>
DEFINE
  Ctautology == Cam2Rev i tautology;
  Cmodality  == Cam2Rev i modality
END
</PRE>
Here are a few tests:<BR>
<PRE>
[ iff [not [or p q]]  [and [not p] [not q]] ]  Ctautology.
true
[ imp [and [imp p q] [imp q r]]  [imp p r] ]  Cmodality.
"tautology"
[ imp [and [imp p q] [imp r q]]  [imp p r] ]  Cmodality.
"contingent"
</PRE>

<A NAME=TOC-6><H2>Other applications</H2></A>
<P>
Testing whether the modal status of a single formula
is not the only thing one might do. 
Another obvious application would be a fixed database as a premise,
and then several queries as conclusions to determine whether
certain facts can be deduced from the database.
Not so obvious would be a reverse example,
which tests, for several inputs, whether a fixed conclusion
follows - and even gives advice accordingly.
<P>
For the advice to be at all meaningful,
the usual single letter atomic formulas are not so intuitive.
It is preferable to use multi-letter formulas,
and their lines in the truth table now have to be defined
as before:
<PRE>
DEFINE 

  raining == ss.s1; windy == ss.s2; cold == ss.s4; 
  hot == ss.s8; humid == ss.s16; 

  badweather == 
    [ raining and windy  or  cold and windy  or 
      raining and cold  or  hot and  humid ] 
END
</PRE>
Since from inconsistent data anything follows,
no advice should be given at all and an appropriate warning
should be supplied.
Also, a warning should be given if the information
was not sufficient to give any kind of advice.
<PRE>
DEFINE
  takeadvice == 
    Min2Rev i 
    [ null ] 
    [ "inconsistent data" ] 
    [ badweather Min2Rev i 
      [ [ [and null] "go out" ] 
        [ [imp not null] "stay home" ] 
        [ "insufficient data" ] ] 
      cond ] 
    ifte 
    popd 
END 
</PRE>
Finally then, here is the glorious application:<BR>
<PRE>
[ raining and not cold and not [humid or raining] ]		takeadvice. 
"inconsistent data"
[ windy and hot and not [hot and not windy] and not raining ]	takeadvice. 
"insufficient data"
[ cold and windy ]						takeadvice. 
"stay home"
[ not [windy or raining or humid] ]				takeadvice. 
"go out"
</PRE>
</BODY>
</HTML>
